(declare-fun zero () (_ FloatingPoint 8 24))
(assert (= zero (_ +zero 8 24)))
(declare-fun one () (_ FloatingPoint 8 24))
(assert (= one ((_ to_fp 8 24) RNE 1.0 0)))
(declare-fun t () (_ FloatingPoint 8 24))
(declare-fun z () (_ FloatingPoint 8 24))
(declare-fun w () (_ FloatingPoint 8 24))
(assert (= w (fp.fma RNE one t one)))
(assert (and (fp.eq z w) (fp.leq zero t) (fp.lt z one)))
(check-sat)
